The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](cs, ncs, node, colorednodes, Cons(x, xs), colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
colorof(S(y96_3), Cons(CN(cl, N(0, adjs)), xs)) →⁺ colorof(S(y96_3), xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(CN(cl, N(0, adjs)), xs)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](cs, ncs, node, colorednodes, Cons(x, xs), colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
colorednoderest[Ite][True][Ite][True][Let]/0
colorednoderest[Ite][True][Ite][True][Let]/1
colorednoderest[Ite][True][Ite][True][Let]/2
colorednoderest[Ite][True][Ite][True][Let]/3
colorednoderest[Ite][True][Ite][True][Let]/4

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
colorof, !EQ, eqColorList, revapp, possible, colorrest, colorednoderest, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
!EQ < colorof
colorof < possible
eqColorList < colorrestthetrick
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
colorrest < colorrestthetrick

(10) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
!EQ, colorof, eqColorList, revapp, possible, colorrest, colorednoderest, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
!EQ < colorof
colorof < possible
eqColorList < colorrestthetrick
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
colorrest < colorrestthetrick

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol !EQ.

(12) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
colorof, eqColorList, revapp, possible, colorrest, colorednoderest, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
colorof < possible
eqColorList < colorrestthetrick
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
colorrest < colorrestthetrick

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colorof.

(14) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
eqColorList, revapp, possible, colorrest, colorednoderest, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
eqColorList < colorrestthetrick
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
colorrest < colorrestthetrick

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

Induction Base:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, 0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_R^Ω(1)
False

Induction Step:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, +(n41_0, 1))), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n41_0, 1))) →_R^Ω(1)
and(True, eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0))) →_IH
and(True, False) →_R^Ω(0)
False

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
revapp, possible, colorrest, colorednoderest, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
colorrest < colorrestthetrick

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)

Induction Base:
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) →_R^Ω(1)
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)

Induction Step:
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, 1)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) →_R^Ω(1)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b))) →_IH
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(+(b, 1), c4056467_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
possible, colorrest, colorednoderest, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
colorrest < colorrestthetrick

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Induction Base:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_R^Ω(1)
True

Induction Step:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4058425_0, 1)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_R^Ω(1)
possible[Ite][True][Ite](eqColor(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), colorof(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0))), gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_R^Ω(1)
possible[Ite][True][Ite](eqColor(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), NoColor), gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_R^Ω(1)
possible[Ite][True][Ite](False, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_R^Ω(0)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →_IH
True

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(22) Complex Obligation (BEST)

(23) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
colornode, colorrest, colorednoderest, colorrestthetrick

They will be analysed ascendingly in the following order:
colorrest = colorednoderest
colorrest < colorrestthetrick

(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colornode.

(25) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
colorednoderest, colorrest, colorrestthetrick

They will be analysed ascendingly in the following order:
colorrest = colorednoderest
colorrest < colorrestthetrick

(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colorednoderest.

(27) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
colorrest, colorrestthetrick

They will be analysed ascendingly in the following order:
colorrest = colorednoderest
colorrest < colorrestthetrick

(28) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colorrest.

(29) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

The following defined symbols remain to be analysed:
colorrestthetrick

(30) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colorrestthetrick.

(31) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(33) BOUNDS(n^1, INF)

(34) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058425_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n4058425₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(36) BOUNDS(n^1, INF)

(37) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056466_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056466_0, b)), rt ∈ Ω(1 + n4056466₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

No more defined symbols left to analyse.

(38) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(39) BOUNDS(n^1, INF)

(40) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]

Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))

No more defined symbols left to analyse.

(41) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(42) BOUNDS(n^1, INF)